A:Type, d1, d2:EqDecider(A), B:(AType), f:a:A fp B(a), x:A, z:B(x). f(x)?z = f(x)?z  B(x) 

latex

Definitions	EqDecider(T), f(x)?z, Top, x. t(x), Unit, , b, a:A fp B(a), x  dom(f), P  Q, P & Q, Prop, b, deq-member(eq;x;L), A, P  Q, False, f(x), x(s), (x  l), x:A. B(x), t  T
Lemmas	l member wf, deq-member wf, assert wf, assert-deq-member, not functionality wrt iff, not wf, bnot wf, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bool wf, fpf-trivial-subtype-top, deq wf, fpf wf